A, B, C:MsgA.
A || B  ma-frame-compat(A;C)  ma-frame-compat(B;C)  ma-frame-compat(A  B;C) 

latex

Definitions

x:A  B(x), P & Q, M1 || M2, M1 ||decl M2, P  Q, x:A. B(x), M1  M2, t  T, x:AB(x), s = t, MsgA, ma-frame-compat(A;B), P  Q, Void, Type, x. t(x), rcv(l,tg), x.A(x), f(x)?z, type List, Valtype(da;k), State(ds), a:A fp B(a), Top, left + right, f  g, mk-ma, , , , s ~ t, {T}, SQType(T), t.2, t.1, IdLnkDeq, KindDeq, IdLnk, Knd, product-deq(A;B;a;b), x  dom(f), b, P  Q, IdDeq, Id, M1  M2, S  T, (x  l), <a, b>, z != f(x)  P(a;z), A, {i..j}, A c B, xdom(f). v=f(x)   P(x;v), M.ds(x), M.dout(l,tg), (s1  s2 mod x), M.da(a), M.state, M.rframe(A.sends tfL of k on l), M.bframe(k sends on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), case b of inl(x) => s(x) | inr(y) => t(y), EqDecider(T), x(s), T, True, False, Atom$n, if b then t else f fi , x:A.B(x), f  g, f(a), f(x), deq-member(eq;x;L), locl(a), suptype(S; T), , map(f;as), a < b, l[i], #$n, {x:A| B(x)} , , i  j < k, A  B, ||as||, [], [car / cdr], i  j , , b, Unit, null(as)

Lemmas

subtype-fpf-cap-void-list, null wf3, equal-nil-lists, void-list-equality3, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool cases, Id sq, length wf nat, nat wf, cons one one, non neg length, le wf, length wf1, int seg wf, select wf, map wf, l member wf, member wf, subtype rel function, subtype rel self, subtype-fpf-cap-void, not wf, locl wf, deq-member wf, bool sq, fpf-ap wf, ma-state-subtype, subtype-fpf-cap-top, ma-sub-join-left, ma-sub wf, ma-sub-join-right, bool wf, id-deq wf, rationals wf, Id wf, fpf-join wf, top wf, IdLnk wf, product-deq wf, Kind-deq wf, idlnk-deq wf, assert wf, fpf-trivial-subtype-top, ma-state wf, ma-valtype wf, pi1 wf, fpf-cap wf, Knd wf, rcv wf, pi2 wf, fpf-join-dom-sq, assert of bor, fpf-dom wf, ma-frame-compat wf, ma-compatible wf, msga wf, ma-join wf